Nuprl Lemma : adjacent-nil
11,40
postcript
pdf
T
:Type,
x
,
y
:
T
. adjacent(
T
;[];
x
;
y
)
False
latex
ProofTree
Definitions
-
n
,
Void
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
{
x
:
A
|
B
(
x
)}
,
{
i
..
j
}
,
Type
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
,
[]
,
#$n
,
n
+
m
,
l
[
i
]
,
,
||
as
||
,
n
-
m
,
(
x
l
)
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
adjacent(
T
;
L
;
x
;
y
)
Lemmas
false
wf
,
int
seg
wf
origin
T:Type, x, y:T. adjacent(T;[];x;y) 
False
T:Type, x, y:T. adjacent(T;[];x;y) False
Q
A
B j < k
}
B(x)
x:A. B(x)
T
l)
B(x)x:A. B(x)